$\forall$${\it es}$:ES, $i$:Id, $P$:(\{$e$:E$\mid$ loc($e$) = $i$\} $\rightarrow$\{$e_{2}$:E$\mid$ loc($e_{2}$) = $i$\} $\rightarrow\mathbb{P}$).
\\[0ex]$\forall$$e_{1}$@$i$. $\forall$$e_{2}$$\geq$$e_{1}$.($\forall$$e$:E. ($e_{1}$ $<$loc $e$) $\Rightarrow$ $e$ $\leq$loc $e_{2}$  $\Rightarrow$ $P$($e$,$e_{2}$)) $\Rightarrow$ $P$($e_{1}$,$e_{2}$)
\\[0ex]$\Rightarrow$ $\forall$$e_{1}$@$i$. $\forall$$e_{2}$$<$$e_{1}$. $P$($e_{1}$,$e_{2}$)
\\[0ex]$\Rightarrow$ ($\forall$$e$, ${\it e'}$:E. (loc($e$) = $i$) $\Rightarrow$ (loc(${\it e'}$) = $i$) $\Rightarrow$ $P$($e$,${\it e'}$))